Nuprl Lemma : grp_op_preserves_le_qorder
11,40
postcript
pdf
x
,
y
,
z
:rationals. qle(
y
;
z
)
qle((
x
+
y
); (
x
+
z
))
latex
Definitions
t
T
,
t
.2
,
t
.1
,
ocgrp{i:l}
,
qadd_grp
,
grp_op(
g
)
,
x
f
y
,
grp_car(
g
)
,
x
:
A
.
B
(
x
)
,
qle(
r
;
s
)
Lemmas
ocgrp
wf
,
qadd
grp
wf2
,
grp
op
preserves
le
origin
x,y,z:rationals. qle(y; z) 
qle((x + y); (x + z)) x,y,z:rationals. qle(y; z) qle((x + y); (x + z)) 
Tx:A. B(x)